1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
use super::*;

/// A simple slice of substitutions
#[derive(Debug, Clone, PartialEq, Eq, Hash, Default)]
pub struct SubstSlice<V, T = ()> {
    /// Terms to substitute the first `n` variables above `base` for
    substs: V,
    /// The base of variables not to substitute
    base: u32,
    /// The typing context for this substitution slice
    ctx: T,
}

impl<V> SubstSlice<V> {
    /// Construct a new substitution vector
    pub fn new(substs: V, base: u32) -> SubstSlice<V> {
        SubstSlice {
            substs,
            base,
            ctx: (),
        }
    }
}

impl<V, T, B> SubstSlice<V, T>
where
    T: TyCtxMut,
    V: Deref<Target = [B]>,
    B: Borrow<TermId>,
{
    /// Construct a new substitution vector, checked in the given context
    pub fn new_with(substs: V, base: u32, mut ctx: T) -> Result<SubstSlice<V, T>, Error> {
        for (i, s) in substs.iter().enumerate() {
            if let Some(annot) = s.borrow().annot() {
                let ty = &*annot.get_ty_id(ctx.cons_ctx());
                if !ctx.constrain(i as u32 + base, ty)?.unwrap_or(true) {
                    return Err(Error::TypeMismatch);
                }
            }
        }
        Ok(SubstSlice { substs, base, ctx })
    }
}

impl<V, T, B> SubstCtx for SubstSlice<V, T>
where
    V: Deref<Target = [B]>,
    T: TyCtxMut,
    B: Borrow<TermId>,
{
    type Ctx = T::MaxDeref;

    #[inline]
    fn subst_var(&mut self, ix: u32, annot: Option<&TermId>) -> Result<Option<TermId>, Error> {
        if let Some(subst_ix) = ix.checked_sub(self.base) {
            let substs = &*self.substs;
            if (subst_ix as usize) < substs.len() {
                let subst: &B = &substs[substs.len() - 1 - subst_ix as usize];
                Ok(Some(subst.borrow().clone()))
            } else {
                let ty = annot.subst_rec(self)?;
                let new_ix = ix - self.substs.len() as u32;
                if ty.is_none() && new_ix == ix {
                    return Ok(None);
                }
                let ty = ty
                    .unwrap_or_else(|| annot.consed(self.ctx.cons_ctx()))
                    .map(|ty| ty.into_shallow_cons(self.ctx.cons_ctx()));
                let term = Var::new_unchecked(new_ix, ty).into_id_with(self.ctx.cons_ctx());
                Ok(Some(term))
            }
        } else if let Some(Some(ty)) = annot.subst_rec(self)? {
            Ok(Some(Var::with_ty(ix, ty).into_id_with(self.ctx.cons_ctx())))
        } else {
            Ok(None)
        }
    }

    #[inline]
    fn push_param(&mut self, param_ty: Option<&TermId>) -> Result<Option<TermId>, Error> {
        let subst = if let Some(param_ty) = param_ty {
            param_ty.subst_id(self)?
        } else {
            None
        };
        self.ctx.push_param(subst.as_ref().or(param_ty))?;
        self.base += 1;
        Ok(subst)
    }

    #[inline]
    fn intersects(&self, filter: VarFilter, _code: Code, _form: Form) -> bool {
        filter.fvb() >= self.base
    }

    #[inline]
    fn ctx(&mut self) -> &mut Self::Ctx {
        self.ctx.ctx()
    }

    #[inline]
    fn pop_param(&mut self) -> Result<(), Error> {
        self.ctx.pop_param()?;
        self.base -= 1;
        Ok(())
    }

    #[inline]
    fn is_var_null(&self) -> bool {
        self.substs.as_ref().is_empty()
    }
}